Termination Proof Script

• Consider the SCC {27,29,30,32-36}. By taking the AF π with π(add) = π(add_active) = π(HD_ACTIVE) = π(incr) = π(incr_active) = π(MARK) = π(s) = π(TL_ACTIVE) = 1 together with the lexicographic path order with precedence hd_active ≻ zeros_active ≻ 0, nats_active ≻ zeros_active ≻ cons, zeros_active ≻ zeros, nats_active ≈ nats and hd_active ≈ tl_active ≈ hd ≈ tl ≈ mark, the rules in {2,4,5,7,10,12-14,16,17,19,29,32,33,35} are weakly decreasing and the rules in {1,3,6,8,9,11,15,18,20,21,27,30,34,36} are strictly decreasing. There is one new SCC.
  • Consider the SCC {29,32}. There are no usable rules. By taking the AF π with π(add) = π(MARK) = 1 together with the lexicographic path order with empty precedence, rule 32 is weakly decreasing and rule 29 is strictly decreasing. There is one new SCC.
    • Consider the SCC {32}. By taking the AF π with π(MARK) = 1 together with the lexicographic path order with empty precedence, rule 32 is strictly decreasing.